-module(pmatch).

-compile(export_all).


%% Implement the recursive unification algorithm from
%% Luger & Stubblefield, p466-7.
%%
%% Now augumented with the stream-based logic programming
%% interpreter from p477-p450.
%%

-define(is_primitive(X), (is_atom(X) orelse is_number(X))).


unify(Foo, Bar) ->
    unify(Foo, Bar, []).


unify(_, _, fail) ->
    fail;
unify({var, P1}, Pattern2, Bindings) ->
    match_var({var, P1}, Pattern2, Bindings);
unify(Pattern1, {var, P2}, Bindings) ->
    match_var({var, P2}, Pattern1, Bindings);
unify(Constant1, Constant1, Bindings) when ?is_primitive(Constant1) ->
    Bindings;
unify(Constant1, _, _) when ?is_primitive(Constant1) ->
    fail;
unify(_, Constant2, _) when ?is_primitive(Constant2) ->
    fail;
unify(Tup1, Tup2, Bindings) when is_tuple(Tup1) andalso is_tuple(Tup2) ->
    unify(tuple_to_list(Tup1), tuple_to_list(Tup2), Bindings);
unify([H1|T1], [H2|T2], Bindings) ->
    unify(T1, T2, unify(H1, H2, Bindings));
unify([], [], Bindings) ->
    Bindings;
unify(_, _, _) ->
    fail.


match_var({var, V}, {var, V}, Bindings) ->
    Bindings;
match_var({var, V}, Pattern, Bindings) ->
    case get_binding(V, Bindings) of
        none ->
            case occurs_in(V, Pattern) of
                true ->
                    fail;
                false ->
                    add_binding(V, Pattern, Bindings)
            end;
        {V, BoundVal} ->
            unify(BoundVal, Pattern, Bindings)
    end.


occurs_in(VarName, {var, VarName}) ->
    true;
occurs_in(_, {var, _}) ->
    false;
occurs_in(_, P) when ?is_primitive(P) ->
    false;
occurs_in(VarName, Tuple) when is_tuple(Tuple) ->
    occurs_in(VarName, tuple_to_list(Tuple));
occurs_in(VarName, [H|T]) ->
    case occurs_in(VarName, H) of
        true -> true;
        false -> occurs_in(VarName, T)
    end;
occurs_in(_, []) ->
    false.


get_binding(Var, Bindings) ->
    proplists:lookup(Var, Bindings).


add_binding(Var, Val, Bindings) ->
    [{Var, Val}|Bindings].



%% Stream processing stuff.  
%% Implementation: stream() = list()
cons_stream(Element, Stream) -> [Element | Stream].


head_stream([H|_]) -> H.


tail_stream([_|T]) -> T.


empty_stream_p([]) -> true;
empty_stream_p([_|_]) -> false.


make_empty_stream() -> [].


combine_stream(Stream1, Stream2) -> Stream1 ++ Stream2.
    
     
%% Logic solver stuff, from 10.8.3.
     

solve(Goal, Substitutions) ->
    case conjunctive_goal_p(Goal) of
        true ->
            filter_through_conj_goals(
              body(Goal),
              cons_stream(Substitutions, make_empty_stream()));
        false ->
            pass
    end.


filter_through_conj_goals([], SubstitutionStream) ->
    SubstitutionStream;
filter_through_conj_goals([Goal|Rest], SubstitutionStream) ->
    filter_through_conj_goals(
      Rest,
      filter_through_goal(Goal, SubstitutionStream)).


filter_through_goal(Goal, SubstitutionStream) ->
    case empty_stream_p(SubstitutionStream) of
        true ->
            make_empty_stream();
        false ->
            combine_streams(
              solve(Goal, head_stream(SubstitutionStream)),
              filter_through_goal(Goal, tail_stream(SubstitutionStream)))
    end.


infer(_Goal, _Subs, []) ->
    make_empty_stream();
infer(Goal, Substitutions, [KBH|KBT]) ->
    Assertion = rename_variables(KBH),
    Match = case rule_p(Assertion) of
                true ->
                    unify(Goal, conclusion(Assertion), Substitutions);
                false ->
                    unify(Goal, Assertion, Substitutions)
            end,
    case Match of
        fail ->
            infer(Goal, Substitutions, KBT);
        _ ->
            case rule_p(Assertion) of
                true ->
                    combine_streams(
                      solve(premise(Assertion), Match),
                      infer(Goal, Substitutions, KBT));
                false ->
                    cons_stream(
                      Match,
                      infer(Goal, Substitutions, KBT))
            end
    end.


rule_p({rule, _, _, _, _}) -> true;
rule_p(_) -> false.


premise({rule, _, P, _, _}) -> P.


conclusion({rule, _, _, _, C}) -> C.


body({goal, _, B}) -> B.


conjunctive_goal_p({goal, 'AND', _}) -> true;
conjunctive_goal_p({goal, _, _}) -> false.


    
    
    
